Nuprl Lemma : es-interface-conditional-domain-member 11,40

es:ES, A:Type, I1I2:AbsInterface(A), e:E.
((e  [I1?I2]))  (((e  I1))  ((e  I2))) 
latex


Definitionsx:AB(x), P  Q, P  Q, P & Q, P  Q, P  Q, t  T, , T, True, P1  P2, P1  P2, {I}
Lemmasassert wf, es-is-interface wf, es-E wf, es-interface wf, event system wf, es-interface-conditional-predicate-equivalent, es-interface-conditional, squash wf, true wf, bool wf, es-interface-conditional-domain, assert of bor

origin